module HOL : sig
  type 'a equal = {equal : 'a -> 'a -> bool}
  val equal : 'a equal -> 'a -> 'a -> bool
  val eq : 'a equal -> 'a -> 'a -> bool
end = struct

type 'a equal = {equal : 'a -> 'a -> bool};;
let equal _A = _A.equal;;

let rec eq _A a b = equal _A a b;;

end;; (*struct HOL*)

module Map : sig
  val map_of : 'a HOL.equal -> ('a * 'b) list -> 'a -> 'b option
end = struct

let rec map_of _A
  x0 k = match x0, k with
    (l, v) :: ps, k -> (if HOL.eq _A l k then Some v else map_of _A ps k)
    | [], k -> None;;

end;; (*struct Map*)

module List : sig
  val map : ('a -> 'b) -> 'a list -> 'b list
  val foldl : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a
  val member : 'a HOL.equal -> 'a list -> 'a -> bool
  val distinct : 'a HOL.equal -> 'a list -> bool
  val list_all : ('a -> bool) -> 'a list -> bool
end = struct

let rec map
  f x1 = match f, x1 with f, [] -> []
    | f, x :: xs -> f x :: map f xs;;

let rec foldl
  f a x2 = match f, a, x2 with f, a, [] -> a
    | f, a, x :: xs -> foldl f (f a x) xs;;

let rec member _A
  x0 y = match x0, y with [], y -> false
    | x :: xs, y -> HOL.eq _A x y || member _A xs y;;

let rec distinct _A
  = function [] -> true
    | x :: xs -> not (member _A xs x) && distinct _A xs;;

let rec list_all
  p x1 = match p, x1 with p, [] -> true
    | p, x :: xs -> p x && list_all p xs;;

end;; (*struct List*)

module Option : sig
  val is_none : 'a option -> bool
  val equal_option : 'a HOL.equal -> 'a option -> 'a option -> bool
end = struct

let rec is_none = function Some x -> false
                  | None -> true;;

let rec equal_option _A
  x0 x1 = match x0, x1 with Some a, None -> false
    | None, Some a -> false
    | Some aa, Some a -> HOL.eq _A aa a
    | None, None -> true;;

end;; (*struct Option*)

module ClangExec : sig
  type vals = BoolV of bool | NatV of Big_int.big_int
  type 'a expr = Evar of 'a | Eimm of vals
  type 'a bexpr = Bex of 'a expr | Beq of 'a expr * 'a expr |
    Bneq of 'a expr * 'a expr
  type ('a, 'b) wcond = Weq of 'b * 'a expr | Wneq of 'b * 'a expr
  type ('a, 'b, 'c, 'd) stmt = Cnone of 'd option |
    Cseq of 'd option * ('a, 'b, 'c, 'd) stmt * ('a, 'b, 'c, 'd) stmt |
    Casg of 'd option * 'b * 'b expr |
    Cif of 'd option * 'b bexpr * ('a, 'b, 'c, 'd) stmt * ('a, 'b, 'c, 'd) stmt
    | Cwhile of 'd option * 'b bexpr * ('a, 'b, 'c, 'd) stmt |
    Cread of 'd option * 'b * 'c | Cwrite of 'd option * 'c * 'b expr |
    Cwait of 'd option * ('b, 'c) wcond list * ('a, 'b, 'c, 'd) stmt
  type val_tp = BoolT | NatT
  type 'a vdecl = Vdecl of 'a * val_tp
  type ('a, 'b, 'c) phdr = Phdr of 'a * 'b vdecl list * 'c vdecl list
  type ('a, 'b, 'c, 'd) proc = Proc of ('a, 'b, 'c) phdr * ('a, 'b, 'c, 'd) stmt
  val vd_name : 'a vdecl -> 'a
  val vd_type : 'a vdecl -> val_tp
  val var_tp : 'a HOL.equal -> 'a vdecl list -> 'a -> val_tp option
  val wt_var : 'a HOL.equal -> 'a vdecl list -> 'a -> bool
  val vals_tp : vals -> val_tp
  val expr_tp : 'a HOL.equal -> 'a vdecl list -> 'a expr -> val_tp option
  val hdr_ctx : ('a, 'b, 'c) phdr -> 'b vdecl list
  val proc_name : ('a, 'b, 'c, 'd) proc -> 'a
  val hdr_ctxsh : ('a, 'b, 'c) phdr -> 'c vdecl list
  val wf_prochdr : 'b HOL.equal -> 'c HOL.equal -> ('a, 'b, 'c, 'd) proc -> bool
  val wt_expr : 'a HOL.equal -> 'a vdecl list -> 'a expr -> bool
  val equal_val_tpa : val_tp -> val_tp -> bool
  val equal_val_tp : val_tp HOL.equal
  val wt_bexpr : 'a HOL.equal -> 'a vdecl list -> 'a bexpr -> bool
  val wt_waitcond :
    'a HOL.equal -> 'b HOL.equal ->
      'a vdecl list -> 'b vdecl list -> ('a, 'b) wcond -> bool
  val wt_waitconds :
    'a HOL.equal -> 'b HOL.equal ->
      'a vdecl list -> 'b vdecl list -> ('a, 'b) wcond list -> bool
  val wt_stmt :
    'a HOL.equal -> 'b HOL.equal ->
      'a vdecl list -> 'b vdecl list -> ('c, 'a, 'b, 'd) stmt -> bool
  val wt_proc : 'b HOL.equal -> 'c HOL.equal -> ('a, 'b, 'c, 'd) proc -> bool
  val is_sub_ctx : 'a HOL.equal -> 'a vdecl list -> 'a vdecl list -> bool
  val is_coh_ctx : 'a HOL.equal -> 'a vdecl list -> 'a vdecl list -> bool
  val proc_ctxsh : ('a, 'b, 'c, 'd) proc -> 'c vdecl list
  val wf_prog :
    'a HOL.equal -> 'b HOL.equal -> 'c HOL.equal ->
      ('a, 'b, 'c, 'd) proc list -> bool
end = struct

type vals = BoolV of bool | NatV of Big_int.big_int;;

type 'a expr = Evar of 'a | Eimm of vals;;

type 'a bexpr = Bex of 'a expr | Beq of 'a expr * 'a expr |
  Bneq of 'a expr * 'a expr;;

type ('a, 'b) wcond = Weq of 'b * 'a expr | Wneq of 'b * 'a expr;;

type ('a, 'b, 'c, 'd) stmt = Cnone of 'd option |
  Cseq of 'd option * ('a, 'b, 'c, 'd) stmt * ('a, 'b, 'c, 'd) stmt |
  Casg of 'd option * 'b * 'b expr |
  Cif of 'd option * 'b bexpr * ('a, 'b, 'c, 'd) stmt * ('a, 'b, 'c, 'd) stmt |
  Cwhile of 'd option * 'b bexpr * ('a, 'b, 'c, 'd) stmt |
  Cread of 'd option * 'b * 'c | Cwrite of 'd option * 'c * 'b expr |
  Cwait of 'd option * ('b, 'c) wcond list * ('a, 'b, 'c, 'd) stmt;;

type val_tp = BoolT | NatT;;

type 'a vdecl = Vdecl of 'a * val_tp;;

type ('a, 'b, 'c) phdr = Phdr of 'a * 'b vdecl list * 'c vdecl list;;

type ('a, 'b, 'c, 'd) proc = Proc of ('a, 'b, 'c) phdr * ('a, 'b, 'c, 'd) stmt;;

let rec vd_name (Vdecl (x, uu)) = x;;

let rec vd_type (Vdecl (uu, tp)) = tp;;

let rec var_tp _A
  ctx v =
    List.foldl
      (fun res vd ->
        (if Option.is_none res && HOL.eq _A (vd_name vd) v
          then Some (vd_type vd) else res))
      None ctx;;

let rec wt_var _A
  ctx e = (match var_tp _A ctx e with None -> false | Some _ -> true);;

let rec vals_tp = function BoolV b -> BoolT
                  | NatV n -> NatT;;

let rec expr_tp _A
  ctx x1 = match ctx, x1 with ctx, Evar v -> var_tp _A ctx v
    | ctx, Eimm i -> Some (vals_tp i);;

let rec hdr_ctx (Phdr (uu, vds, uv)) = vds;;

let rec proc_name (Proc (Phdr (nm, uu, uv), uw)) = nm;;

let rec hdr_ctxsh (Phdr (uu, uv, vds)) = vds;;

let rec wf_prochdr _B _C
  (Proc (hdr, s)) =
    List.distinct _B (List.map vd_name (hdr_ctx hdr)) &&
      List.distinct _C (List.map vd_name (hdr_ctxsh hdr));;

let rec wt_expr _A
  ctx e = (match expr_tp _A ctx e with None -> false | Some _ -> true);;

let rec equal_val_tpa
  x0 x1 = match x0, x1 with NatT, BoolT -> false
    | BoolT, NatT -> false
    | NatT, NatT -> true
    | BoolT, BoolT -> true;;

let equal_val_tp = ({HOL.equal = equal_val_tpa} : val_tp HOL.equal);;

let rec wt_bexpr _A
  ctx x1 = match ctx, x1 with
    ctx, Bex e ->
      (match expr_tp _A ctx e with None -> false | Some BoolT -> true
        | Some NatT -> false)
    | ctx, Beq (e1, e2) ->
        wt_expr _A ctx e1 &&
          Option.equal_option equal_val_tp (expr_tp _A ctx e1)
            (expr_tp _A ctx e2)
    | ctx, Bneq (e1, e2) ->
        wt_expr _A ctx e1 &&
          Option.equal_option equal_val_tp (expr_tp _A ctx e1)
            (expr_tp _A ctx e2);;

let rec wt_waitcond _A _B
  loc sh x2 = match loc, sh, x2 with
    loc, sh, Weq (x, e) ->
      wt_var _B sh x &&
        (wt_expr _A loc e &&
          Option.equal_option equal_val_tp (var_tp _B sh x) (expr_tp _A loc e))
    | loc, sh, Wneq (x, e) ->
        wt_var _B sh x &&
          (wt_expr _A loc e &&
            Option.equal_option equal_val_tp (var_tp _B sh x)
              (expr_tp _A loc e));;

let rec wt_waitconds _A _B
  loc sh wcs = List.list_all (wt_waitcond _A _B loc sh) wcs;;

let rec wt_stmt _A _B
  loc sh x2 = match loc, sh, x2 with loc, sh, Cnone uu -> true
    | loc, sh, Cseq (uv, s1, s2) ->
        wt_stmt _A _B loc sh s1 && wt_stmt _A _B loc sh s2
    | loc, sh, Casg (uw, x, e) ->
        wt_var _A loc x &&
          (wt_expr _A loc e &&
            Option.equal_option equal_val_tp (var_tp _A loc x)
              (expr_tp _A loc e))
    | loc, sh, Cif (ux, be, s1, s2) ->
        wt_bexpr _A loc be &&
          (wt_stmt _A _B loc sh s1 && wt_stmt _A _B loc sh s2)
    | loc, sh, Cwhile (uy, be, s) ->
        wt_bexpr _A loc be && wt_stmt _A _B loc sh s
    | loc, sh, Cread (uz, u, v) ->
        wt_var _A loc u &&
          (wt_var _B sh v &&
            Option.equal_option equal_val_tp (var_tp _A loc u) (var_tp _B sh v))
    | loc, sh, Cwrite (va, u, e) ->
        wt_var _B sh u &&
          (wt_expr _A loc e &&
            Option.equal_option equal_val_tp (var_tp _B sh u)
              (expr_tp _A loc e))
    | loc, sh, Cwait (vb, wcs, s) ->
        wt_waitconds _A _B loc sh wcs && wt_stmt _A _B loc sh s;;

let rec wt_proc _B _C
  (Proc (hdr, s)) = wt_stmt _B _C (hdr_ctx hdr) (hdr_ctxsh hdr) s;;

let rec is_sub_ctx _A
  ctx1 ctx2 =
    List.list_all
      (fun vd ->
        Option.is_none (var_tp _A ctx2 (vd_name vd)) ||
          Option.equal_option equal_val_tp (var_tp _A ctx2 (vd_name vd))
            (Some (vd_type vd)))
      ctx1;;

let rec is_coh_ctx _A
  ctx1 ctx2 = is_sub_ctx _A ctx1 ctx2 && is_sub_ctx _A ctx2 ctx1;;

let rec proc_ctxsh (Proc (hdr, uu)) = hdr_ctxsh hdr;;

let rec wf_prog _A _B _C
  prog =
    List.distinct _A (List.map proc_name prog) &&
      (List.list_all (fun proc -> wf_prochdr _B _C proc && wt_proc _B _C proc)
         prog &&
        List.list_all
          (fun proc1 ->
            List.list_all
              (fun proc2 -> is_coh_ctx _C (proc_ctxsh proc1) (proc_ctxsh proc2))
              prog)
          prog);;

end;; (*struct ClangExec*)
